\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $i$:${\it ff}$.C, $e$:\{$e$:E$\mid$ ${\it ff}$.R($i$,$e$)\} , $j$:\{$j$:${\it ff}$.C$\mid$ ${\it ff}$.S($j$,$i$,${\it ff}$.Sender($i$,$e$))\} .
\\[0ex]($\forall$$i$, $j$:${\it ff}$.C, $e$:E. Dec(${\it ff}$.S($i$,$j$,$e$)))
\\[0ex]$\Rightarrow$ (\=${\it ff}$.Decodes($i$,$e$,(state when $e$))\+
\\[0ex]=
\\[0ex]${\it ff}$.Codes($j$,$i$,${\it ff}$.Sender($i$,$e$),(state when ${\it ff}$.Sender($i$,$e$)))
\\[0ex]$\in$ ${\it ff}$.T)
\-
\end{tabbing}